$\forall$$A$:Type, $L$:($A$ List), $i$:Id, $R$:(\{$a$:$A$$\mid$ ($a$ $\in$ $L$)\} $\rightarrow$Realizer).
\\[0ex]($\uparrow$R{-}has{-}loc($\oplus$$x$$\in$$L$.$R$($x$);$i$)) $\Leftarrow\!\Rightarrow$ ($\exists$$x$$\in$$L$.$\uparrow$R{-}has{-}loc($R$($x$);$i$))